Nuprl Definition : es-p-locl
11,40
postcript
pdf
e
p
<
e'
==
n
:
. (p-graph(E;
p
^
n
)(
e'
,
e
))
latex
clarification:
es-p-locl(
es
;
p
;
e
;
e'
) ==
n
:
. (p-graph(es-E(
es
);
p
^
n
)(
e'
,
e
))
latex
Definitions
x
:
A
.
B
(
x
)
,
,
f
(
a
)
,
p-graph(
A
;
f
)
,
E
,
f
^
n
FDL editor aliases
es-p-locl
origin
n:
. (p-graph(E;p^n)(e',e))
n:. (p-graph(es-E(es);p^n)(e',e)) n:. (p-graph(E;p^n)(e',e))
n:. (p-graph(es-E(es);p^n)(e',e)) x:A. B(x)